Theorem rexbidva 2494

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

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

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-rex 2481

This theorem is referenced by:  2rexbiia  2513  2rexbidva  2520  rexeqbidva  2712  dfimafn  5612  funimass4  5614  fconstfvm  5783  fliftel  5843  fliftf  5849  f1oiso  5876  releldm2  6252  frecabcl  6466  qsinxp  6679  qliftel  6683  supisolem  7083  enumctlemm  7189  ismkvnex  7230  genpassl  7610  genpassu  7611  addcomprg  7664  mulcomprg  7666  1idprl  7676  1idpru  7677  archrecnq  7749  archrecpr  7750  caucvgprprlemexbt  7792  caucvgprprlemexb  7793  archsr  7868  map2psrprg  7891  suplocsrlempr  7893  axsuploc  8118  cnegexlem3  8222  cnegex2  8224  recexre  8624  rerecclap  8776  creur  9005  creui  9006  nndiv  9050  arch  9265  nnrecl  9266  expnlbnd  10775  fimaxq  10938  wrdval  10957  clim2  11467  clim2c  11468  clim0c  11470  climabs0  11491  climrecvg1n  11532  sumeq2  11543  mertensabs  11721  prodeq2  11741  zproddc  11763  nndivides  11981  alzdvds  12038  oddm1even  12059  oddnn02np1  12064  oddge22np1  12065  evennn02n  12066  evennn2n  12067  divalgb  12109  modremain  12113  modprmn0modprm0  12452  pythagtriplem2  12462  pythagtrip  12479  pceu  12491  4sqlem12  12598  gsumpropd2  13097  mndpfo  13142  mndpropd  13144  grppropd  13221  conjnmzb  13488  dvdsr02  13739  crngunit  13745  dvdsrpropdg  13781  cnfldui  14223  znunit  14293  iscnp3  14547  lmbrf  14559  cncnp  14574  lmss  14590  metrest  14850  metcnp  14856  metcnp2  14857  txmetcnp  14862  cdivcncfap  14948  ivthdec  14988  lgsquadlem2  15427  2lgslem1a  15437  pw1nct  15758