ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-i11e Unicode version

Axiom ax-i11e 1269
Description: Axiom of Variable Substitution for Existence. This can be derived from ax-11 1268 in a classical context but a separate axiom is needed for intuitionistic predicate calculus. (Contributed by Mario Carneiro, 31-Jan-2015.) (Revised by Mario Carneiro and Jim Kingdon, 31-Dec-2017.)
Assertion
Ref Expression
ax-i11e

Detailed syntax breakdown of Axiom ax-i11e
StepHypRef Expression
1 vx . . 3
2 vy . . 3
31, 2weq 1263 . 2
4 wph . . . . 5
53, 4wa 95 . . . 4
65, 1wex 1253 . . 3
74, 2wex 1253 . . 3
86, 7wi 4 . 2
93, 8wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  ax10oe  1412  drex1  1420  sbcof2  1477  ax11ev  1570
  Copyright terms: Public domain W3C validator