Theorem rexbidva 2434

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

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

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-rex 2422

This theorem is referenced by:  2rexbiia  2451  2rexbidva  2458  rexeqbidva  2641  dfimafn  5470  funimass4  5472  fconstfvm  5638  fliftel  5694  fliftf  5700  f1oiso  5727  releldm2  6083  frecabcl  6296  qsinxp  6505  qliftel  6509  supisolem  6895  enumctlemm  6999  ismkvnex  7029  genpassl  7332  genpassu  7333  addcomprg  7386  mulcomprg  7388  1idprl  7398  1idpru  7399  archrecnq  7471  archrecpr  7472  caucvgprprlemexbt  7514  caucvgprprlemexb  7515  archsr  7590  map2psrprg  7613  suplocsrlempr  7615  axsuploc  7837  cnegexlem3  7939  cnegex2  7941  recexre  8340  rerecclap  8490  creur  8717  creui  8718  nndiv  8761  arch  8974  nnrecl  8975  expnlbnd  10416  fimaxq  10573  clim2  11052  clim2c  11053  clim0c  11055  climabs0  11076  climrecvg1n  11117  sumeq2  11128  mertensabs  11306  prodeq2  11326  nndivides  11500  alzdvds  11552  oddm1even  11572  oddnn02np1  11577  oddge22np1  11578  evennn02n  11579  evennn2n  11580  divalgb  11622  modremain  11626  iscnp3  12372  lmbrf  12384  cncnp  12399  lmss  12415  metrest  12675  metcnp  12681  metcnp2  12682  txmetcnp  12687  cdivcncfap  12756  ivthdec  12791