Theorem 2ralbidv 2988

Description: Formula-building rule for restricted universal quantifiers (deduction rule). (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 2985	. 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
3	2	ralbidv 2985	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 196  ∀wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841

This theorem depends on definitions:  df-bi 197  df-an 386  df-ral 2917

This theorem is referenced by:  cbvral3v  3174  ralxpxfr2d  3316  poeq1  5003  soeq1  5019  isoeq1  6522  isoeq2  6523  isoeq3  6524  fnmpt2ovd  7198  smoeq  7393  xpf1o  8067  nqereu  9696  dedekind  10145  dedekindle  10146  seqcaopr2  12774  wrd2ind  13410  addcn2  14253  mulcn2  14255  mreexexd  16224  mreexexdOLD  16225  catlid  16260  catrid  16261  isfunc  16440  funcres2b  16473  isfull  16486  isfth  16490  fullres2c  16515  isnat  16523  evlfcl  16778  uncfcurf  16795  isprs  16846  isdrs  16850  ispos  16863  istos  16951  isdlat  17109  sgrp1  17209  ismhm  17253  issubm  17263  sgrp2nmndlem4  17331  isnsg  17539  isghm  17576  isga  17640  pmtrdifwrdel  17821  sylow2blem2  17952  efglem  18045  efgi  18048  efgredlemb  18075  efgred  18077  frgpuplem  18101  iscmn  18116  ring1  18518  isirred  18615  islmod  18783  lmodlema  18784  lssset  18848  islssd  18850  islmhm  18941  islmhm2  18952  isobs  19978  dmatel  20213  dmatmulcl  20220  scmateALT  20232  mdetunilem3  20334  mdetunilem4  20335  mdetunilem9  20340  cpmatel  20430  chpscmat  20561  hausnei2  21062  dfconn2  21127  llyeq  21178  nllyeq  21179  isucn2  21988  iducn  21992  ispsmet  22014  ismet  22033  isxmet  22034  metucn  22281  ngptgp  22345  nlmvscnlem1  22395  xmetdcn2  22543  addcnlem  22570  elcncf  22595  ipcnlem1  22947  cfili  22969  c1lip1  23659  aalioulem5  23990  aalioulem6  23991  aaliou  23992  aaliou2  23994  aaliou2b  23995  ulmcau  24048  ulmdvlem3  24055  cxpcn3lem  24383  dvdsmulf1o  24815  chpdifbndlem2  25138  pntrsumbnd2  25151  istrkgb  25249  axtgsegcon  25258  axtg5seg  25259  axtgpasch  25261  axtgeucl  25266  iscgrg  25302  isismt  25324  isperp2  25505  f1otrg  25646  axcontlem10  25748  axcontlem12  25750  isgrpo  27191  isablo  27240  vacn  27389  smcnlem  27392  lnoval  27447  islno  27448  isphg  27512  ajmoi  27554  ajval  27557  adjmo  28531  elcnop  28556  ellnop  28557  elunop  28571  elhmop  28572  elcnfn  28581  ellnfn  28582  adjeu  28588  adjval  28589  adj1  28632  adjeq  28634  cnlnadjlem9  28774  cnlnadjeu  28777  cnlnssadj  28779  isst  28912  ishst  28913  cdj1i  29132  cdj3i  29140  resspos  29436  resstos  29437  isomnd  29478  isslmd  29532  slmdlema  29533  isorng  29576  qqhucn  29810  ismntop  29844  axtgupdim2OLD  30445  txpconn  30914  nn0prpw  31952  heicant  33062  equivbnd  33207  isismty  33218  heibor1lem  33226  iccbnd  33257  isass  33263  elghomlem1OLD  33302  elghomlem2OLD  33303  isrngohom  33382  iscom2  33412  pridlval  33450  ispridl  33451  isdmn3  33491  islfl  33813  isopos  33933  psubspset  34496  islaut  34835  ispautN  34851  ltrnset  34870  isltrn  34871  istrnN  34910  istendo  35514  clsk1independent  37812  sprsymrelfolem2  41018  sprsymrelfo  41022  ismgmhm  41044  issubmgm  41050  isrnghm  41153  lidlmsgrp  41187  lidlrng  41188  dmatALTbasel  41453  lindslinindsimp2  41514  lmod1  41543