Theorem reeanv 2634

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 1516	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1516	. 2 ⊢ Ⅎ𝑥𝜓
3	1, 2	reean 2633	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓))

Syntax hints:   ∧ wa 103   ↔ wb 104  ∃wrex 2444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-cleq 2158  df-clel 2161  df-nfc 2296  df-rex 2449

This theorem is referenced by:  3reeanv  2635  fliftfun  5763  tfrlem5  6278  eroveu  6588  erovlem  6589  xpf1o  6806  genprndl  7458  genprndu  7459  ltpopr  7532  ltsopr  7533  cauappcvgprlemdisj  7588  caucvgprlemdisj  7611  caucvgprprlemdisj  7639  exbtwnzlemex  10181  rebtwn2z  10186  rexanre  11158  summodc  11320  prodmodclem2  11514  prodmodc  11515  dvds2lem  11739  odd2np1  11806  opoe  11828  omoe  11829  opeo  11830  omeo  11831  gcddiv  11948  divgcdcoprmex  12030  pcqmul  12231  pcadd  12267  mul4sq  12320  tgcl  12664  restbasg  12768  txuni2  12856  txbas  12858  txcnp  12871  blin2  13032  tgqioo  13147  mul2sq  13552  2sqlem5  13555