Theorem rexbidva 2474

Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 9-Mar-1997.)

Hypothesis

Ref	Expression
ralbidva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rexbidva	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rexbidva

Step	Hyp	Ref	Expression
1		nfv 1528	. 2 ⊢ Ⅎ𝑥𝜑
2		ralbidva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	1, 2	rexbida 2472	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∈ wcel 2148  ∃wrex 2456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-rex 2461

This theorem is referenced by:  2rexbiia  2493  2rexbidva  2500  rexeqbidva  2687  dfimafn  5564  funimass4  5566  fconstfvm  5734  fliftel  5793  fliftf  5799  f1oiso  5826  releldm2  6185  frecabcl  6399  qsinxp  6610  qliftel  6614  supisolem  7006  enumctlemm  7112  ismkvnex  7152  genpassl  7522  genpassu  7523  addcomprg  7576  mulcomprg  7578  1idprl  7588  1idpru  7589  archrecnq  7661  archrecpr  7662  caucvgprprlemexbt  7704  caucvgprprlemexb  7705  archsr  7780  map2psrprg  7803  suplocsrlempr  7805  axsuploc  8028  cnegexlem3  8132  cnegex2  8134  recexre  8533  rerecclap  8685  creur  8914  creui  8915  nndiv  8958  arch  9171  nnrecl  9172  expnlbnd  10641  fimaxq  10802  clim2  11286  clim2c  11287  clim0c  11289  climabs0  11310  climrecvg1n  11351  sumeq2  11362  mertensabs  11540  prodeq2  11560  zproddc  11582  nndivides  11799  alzdvds  11854  oddm1even  11874  oddnn02np1  11879  oddge22np1  11880  evennn02n  11881  evennn2n  11882  divalgb  11924  modremain  11928  modprmn0modprm0  12250  pythagtriplem2  12260  pythagtrip  12277  pceu  12289  mndpfo  12833  mndpropd  12835  grppropd  12887  dvdsr02  13267  crngunit  13273  dvdsrpropdg  13309  iscnp3  13634  lmbrf  13646  cncnp  13661  lmss  13677  metrest  13937  metcnp  13943  metcnp2  13944  txmetcnp  13949  cdivcncfap  14018  ivthdec  14053  pw1nct  14672