Theorem 2ralbidv 3202

Description: Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.)

Hypothesis

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

Assertion

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

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

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

Proof of Theorem 2ralbidv

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3045

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-ral 3046

This theorem is referenced by:  3ralbidv  3205  6ralbidv  3207  cbvral3vw  3222  cbvral6vw  3224  cbvral3v  3346  rspc6v  3612  ralxpxfr2d  3615  poeq1  5552  soeq1  5570  isoeq1  7295  isoeq2  7296  isoeq3  7297  fnmpoovd  8069  xpord3inddlem  8136  smoeq  8322  xpf1o  9109  nqereu  10889  dedekind  11344  dedekindle  11345  seqcaopr2  14010  wrd2ind  14695  addcn2  15567  mulcn2  15569  mreexexd  17616  catlid  17651  catrid  17652  isfunc  17833  funcres2b  17866  isfull  17881  isfth  17885  fullres2c  17910  isnat  17919  evlfcl  18190  uncfcurf  18207  isprs  18264  isdrs  18269  ispos  18282  istos  18384  isdlat  18488  ismgmhm  18630  issubmgm  18636  sgrp1  18663  ismhm  18719  issubm  18737  sgrp2nmndlem4  18862  isnsg  19094  isghm  19154  isghmOLD  19155  isga  19230  pmtrdifwrdel  19422  sylow2blem2  19558  efglem  19653  efgi  19656  efgredlemb  19683  efgred  19685  frgpuplem  19709  iscmn  19726  ring1  20226  isirred  20335  rnghmval  20356  isrnghm  20357  islmod  20777  lmodlema  20778  lssset  20846  islssd  20848  islmhm  20941  islmhm2  20952  isobs  21636  dmatel  22387  dmatmulcl  22394  scmateALT  22406  mdetunilem3  22508  mdetunilem4  22509  mdetunilem9  22514  cpmatel  22605  chpscmat  22736  hausnei2  23247  dfconn2  23313  llyeq  23364  nllyeq  23365  isucn2  24173  iducn  24177  ispsmet  24199  ismet  24218  isxmet  24219  metucn  24466  ngptgp  24531  nlmvscnlem1  24581  xmetdcn2  24733  addcnlem  24760  elcncf  24789  ipcnlem1  25152  cfili  25175  c1lip1  25909  aalioulem5  26251  aalioulem6  26252  aaliou  26253  aaliou2  26255  aaliou2b  26256  ulmcau  26311  ulmdvlem3  26318  cxpcn3lem  26664  mpodvdsmulf1o  27111  dvdsmulf1o  27113  chpdifbndlem2  27472  pntrsumbnd2  27485  addsprop  27890  negsprop  27948  istrkgb  28389  axtgsegcon  28398  axtg5seg  28399  axtgpasch  28401  axtgeucl  28406  iscgrg  28446  isismt  28468  isperp2  28649  f1otrg  28805  axcontlem10  28907  axcontlem12  28909  iscusgredg  29357  isgrpo  30433  isablo  30482  vacn  30630  smcnlem  30633  lnoval  30688  islno  30689  isphg  30753  ajmoi  30794  ajval  30797  adjmo  31768  elcnop  31793  ellnop  31794  elunop  31808  elhmop  31809  elcnfn  31818  ellnfn  31819  adjeu  31825  adjval  31826  adj1  31869  adjeq  31871  cnlnadjlem9  32011  cnlnadjeu  32014  cnlnssadj  32016  isst  32149  ishst  32150  cdj1i  32369  cdj3i  32377  resspos  32899  resstos  32900  ismnt  32916  mgcval  32920  isomnd  33022  isslmd  33162  slmdlema  33163  isorng  33284  prmidlval  33415  isprmidl  33416  isrprm  33495  qqhucn  33989  ismntop  34023  axtgupdim2ALTV  34666  txpconn  35226  nn0prpw  36318  heicant  37656  equivbnd  37791  isismty  37802  heibor1lem  37810  iccbnd  37841  isass  37847  elghomlem1OLD  37886  elghomlem2OLD  37887  isrngohom  37966  iscom2  37996  pridlval  38034  ispridl  38035  isdmn3  38075  inecmo  38344  islfl  39060  isopos  39180  psubspset  39745  islaut  40084  ispautN  40100  ltrnset  40119  isltrn  40120  istrnN  40158  istendo  40761  sticksstones1  42141  sticksstones2  42142  sticksstones3  42143  sticksstones8  42148  sticksstones10  42150  sticksstones11  42151  sticksstones12a  42152  sticksstones15  42156  sn-isghm  42668  clsk1independent  44042  relpeq1  44941  relpeq2  44942  relpeq3  44943  sprsymrelfolem2  47498  sprsymrelfo  47502  reuopreuprim  47531  dmatALTbasel  48395  lindslinindsimp2  48456  lmod1  48485  isnrm4  48923  iscnrm4  48946  isuplem  49172  isthinc  49412  thincciso  49446  thinccisod  49447