 Kripke does not discuss the details of Prior’s proof. Prior’s proof for the Barcan formula adopts Łukasiewicz’s rules for the introduction of the existential quantifier. The second of these rules states that if \(\mvdash A\rightarrow B\) then \(\mvdash A\rightarrow(\exists x)B\). Prior applies the rule to 