NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  rexeq GIF version

Theorem rexeq 2808
Description: Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.)
Assertion
Ref Expression
rexeq (A = B → (x A φx B φ))
Distinct variable groups:   x,A   x,B
Allowed substitution hint:   φ(x)

Proof of Theorem rexeq
StepHypRef Expression
1 nfcv 2489 . 2 xA
2 nfcv 2489 . 2 xB
31, 2rexeqf 2804 1 (A = B → (x A φx B φ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176   = wceq 1642  wrex 2615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-cleq 2346  df-clel 2349  df-nfc 2478  df-rex 2620
This theorem is referenced by:  rexeqi  2812  rexeqdv  2814  rexeqbi1dv  2816  unieq  3900  xpkeq1  4198  xpkeq2  4199  imakeq2  4225  tfineq  4488  nnadjoin  4520  tfinnn  4534  imaeq2  4938  qseq1  5974  brlecg  6112  ovmuc  6130  tceq  6158  lec0cg  6198  sbth  6206  dflec3  6221  lenc  6223
  Copyright terms: Public domain W3C validator