Theorem reeanv 2646

Description: Rearrange existential quantifiers. (Contributed by NM, 9-May-1999.)

Assertion

Ref	Expression
reeanv	⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓))

Distinct variable groups:   𝜑,𝑦   𝜓,𝑥   𝑥,𝑦   𝑦,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)   𝐴(𝑥)   𝐵(𝑦)

Proof of Theorem reeanv

Step	Hyp	Ref	Expression
1		nfv 1528	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1528	. 2 ⊢ Ⅎ𝑥𝜓
3	1, 2	reean 2645	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓))

Syntax hints:   ∧ wa 104   ↔ wb 105  ∃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-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461

This theorem is referenced by:  3reeanv  2647  fliftfun  5796  tfrlem5  6314  eroveu  6625  erovlem  6626  xpf1o  6843  genprndl  7519  genprndu  7520  ltpopr  7593  ltsopr  7594  cauappcvgprlemdisj  7649  caucvgprlemdisj  7672  caucvgprprlemdisj  7700  exbtwnzlemex  10249  rebtwn2z  10254  rexanre  11228  summodc  11390  prodmodclem2  11584  prodmodc  11585  dvds2lem  11809  odd2np1  11877  opoe  11899  omoe  11900  opeo  11901  omeo  11902  gcddiv  12019  divgcdcoprmex  12101  pcqmul  12302  pcadd  12338  mul4sq  12391  dvdsrtr  13268  unitgrp  13283  tgcl  13534  restbasg  13638  txuni2  13726  txbas  13728  txcnp  13741  blin2  13902  tgqioo  14017  mul2sq  14433  2sqlem5  14436