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  2688  dfimafn  5566  funimass4  5568  fconstfvm  5736  fliftel  5796  fliftf  5802  f1oiso  5829  releldm2  6188  frecabcl  6402  qsinxp  6613  qliftel  6617  supisolem  7009  enumctlemm  7115  ismkvnex  7155  genpassl  7525  genpassu  7526  addcomprg  7579  mulcomprg  7581  1idprl  7591  1idpru  7592  archrecnq  7664  archrecpr  7665  caucvgprprlemexbt  7707  caucvgprprlemexb  7708  archsr  7783  map2psrprg  7806  suplocsrlempr  7808  axsuploc  8032  cnegexlem3  8136  cnegex2  8138  recexre  8537  rerecclap  8689  creur  8918  creui  8919  nndiv  8962  arch  9175  nnrecl  9176  expnlbnd  10647  fimaxq  10809  clim2  11293  clim2c  11294  clim0c  11296  climabs0  11317  climrecvg1n  11358  sumeq2  11369  mertensabs  11547  prodeq2  11567  zproddc  11589  nndivides  11806  alzdvds  11862  oddm1even  11882  oddnn02np1  11887  oddge22np1  11888  evennn02n  11889  evennn2n  11890  divalgb  11932  modremain  11936  modprmn0modprm0  12258  pythagtriplem2  12268  pythagtrip  12285  pceu  12297  mndpfo  12844  mndpropd  12846  grppropd  12898  dvdsr02  13279  crngunit  13285  dvdsrpropdg  13321  iscnp3  13742  lmbrf  13754  cncnp  13769  lmss  13785  metrest  14045  metcnp  14051  metcnp2  14052  txmetcnp  14057  cdivcncfap  14126  ivthdec  14161  pw1nct  14791