Theorem rexbidva 2451

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 1505	. 2 ⊢ Ⅎ𝑥𝜑
2		ralbidva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	1, 2	rexbida 2449	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∈ wcel 2125  ∃wrex 2433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1487  ax-17 1503  ax-ial 1511

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-rex 2438

This theorem is referenced by:  2rexbiia  2470  2rexbidva  2477  rexeqbidva  2664  dfimafn  5510  funimass4  5512  fconstfvm  5678  fliftel  5734  fliftf  5740  f1oiso  5767  releldm2  6123  frecabcl  6336  qsinxp  6545  qliftel  6549  supisolem  6940  enumctlemm  7044  ismkvnex  7077  genpassl  7423  genpassu  7424  addcomprg  7477  mulcomprg  7479  1idprl  7489  1idpru  7490  archrecnq  7562  archrecpr  7563  caucvgprprlemexbt  7605  caucvgprprlemexb  7606  archsr  7681  map2psrprg  7704  suplocsrlempr  7706  axsuploc  7929  cnegexlem3  8031  cnegex2  8033  recexre  8432  rerecclap  8582  creur  8809  creui  8810  nndiv  8853  arch  9066  nnrecl  9067  expnlbnd  10520  fimaxq  10678  clim2  11157  clim2c  11158  clim0c  11160  climabs0  11181  climrecvg1n  11222  sumeq2  11233  mertensabs  11411  prodeq2  11431  zproddc  11453  nndivides  11667  alzdvds  11719  oddm1even  11739  oddnn02np1  11744  oddge22np1  11745  evennn02n  11746  evennn2n  11747  divalgb  11789  modremain  11793  iscnp3  12542  lmbrf  12554  cncnp  12569  lmss  12585  metrest  12845  metcnp  12851  metcnp2  12852  txmetcnp  12857  cdivcncfap  12926  ivthdec  12961  pw1nct  13514