Theorem rexralbidv 3223

Description: Formula-building rule for restricted quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.)

Hypothesis

Ref	Expression
2ralbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rexralbidv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem rexralbidv

Step	Hyp	Ref	Expression
1		2ralbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	ralbidv 3178	. 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
3	2	rexbidv 3179	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3061  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3062  df-rex 3071

This theorem is referenced by:  freq1  5652  rexfiuz  15386  cau3lem  15393  caubnd2  15396  climi  15546  rlimi  15549  o1lo1  15573  2clim  15608  lo1le  15688  caucvgrlem  15709  caurcvgr  15710  caucvgb  15716  vdwlem10  17028  vdwlem13  17031  pmatcollpw2lem  22783  neiptopnei  23140  lmcvg  23270  lmss  23306  elpt  23580  elptr  23581  txlm  23656  tsmsi  24142  ustuqtop4  24253  isucn  24287  isucn2  24288  ucnima  24290  metcnpi  24557  metcnpi2  24558  metucn  24584  xrge0tsms  24856  elcncf  24915  cncfi  24920  lmmcvg  25295  lhop1  26053  ulmval  26423  ulmi  26429  ulmcaulem  26437  ulmdvlem3  26445  pntibnd  27637  pntlem3  27653  pntleml  27655  axtgcont1  28476  perpln1  28718  perpln2  28719  isperp  28720  brbtwn  28914  uvtx01vtx  29414  isgrpo  30516  ubthlem3  30891  ubth  30892  hcau  31203  hcaucvg  31205  hlimi  31207  hlimconvi  31210  hlim2  31211  elcnop  31876  elcnfn  31901  cnopc  31932  cnfnc  31949  lnopcon  32054  lnfncon  32075  riesz1  32084  xrge0tsmsd  33065  signsply0  34566  unblimceq0  36508  cvgcau  45501  limcleqr  45659  addlimc  45663  0ellimcdiv  45664  climd  45687  climisp  45761  lmbr3  45762  climrescn  45763  climxrrelem  45764  climxrre  45765  xlimpnfxnegmnf  45829  xlimxrre  45846  xlimmnf  45856  xlimpnf  45857  xlimmnfmpt  45858  xlimpnfmpt  45859  dfxlim2  45863  cncfshift  45889  cncfperiod  45894  ioodvbdlimc1lem1  45946  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  fourierdlem68  46189  fourierdlem87  46208  fourierdlem103  46224  fourierdlem104  46225  etransclem48  46297