MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iunopab Structured version   Visualization version   GIF version

Theorem iunopab 5116
Description: Move indexed union inside an ordered-pair abstraction. (Contributed by Stefan O'Rear, 20-Feb-2015.)
Assertion
Ref Expression
iunopab 𝑧𝐴 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐴 𝜑}
Distinct variable groups:   𝑥,𝐴   𝑦,𝐴   𝑦,𝑧   𝑥,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)   𝐴(𝑧)

Proof of Theorem iunopab
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 elopab 5087 . . . . 5 (𝑤 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
21rexbii 3143 . . . 4 (∃𝑧𝐴 𝑤 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑧𝐴𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
3 rexcom4 3329 . . . . 5 (∃𝑧𝐴𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑥𝑧𝐴𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
4 rexcom4 3329 . . . . . . 7 (∃𝑧𝐴𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑦𝑧𝐴 (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
5 r19.42v 3194 . . . . . . . 8 (∃𝑧𝐴 (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑧𝐴 𝜑))
65exbii 1887 . . . . . . 7 (∃𝑦𝑧𝐴 (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑧𝐴 𝜑))
74, 6bitri 264 . . . . . 6 (∃𝑧𝐴𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑧𝐴 𝜑))
87exbii 1887 . . . . 5 (∃𝑥𝑧𝐴𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑧𝐴 𝜑))
93, 8bitri 264 . . . 4 (∃𝑧𝐴𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑧𝐴 𝜑))
102, 9bitri 264 . . 3 (∃𝑧𝐴 𝑤 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑧𝐴 𝜑))
1110abbii 2841 . 2 {𝑤 ∣ ∃𝑧𝐴 𝑤 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}} = {𝑤 ∣ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑧𝐴 𝜑)}
12 df-iun 4630 . 2 𝑧𝐴 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑧𝐴 𝑤 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}}
13 df-opab 4821 . 2 {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐴 𝜑} = {𝑤 ∣ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑧𝐴 𝜑)}
1411, 12, 133eqtr4i 2756 1 𝑧𝐴 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐴 𝜑}
Colors of variables: wff setvar class
Syntax hints:  wa 383   = wceq 1596  wex 1817  wcel 2103  {cab 2710  wrex 3015  cop 4291   ciun 4628  {copab 4820
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pr 5011
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ral 3019  df-rex 3020  df-v 3306  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-sn 4286  df-pr 4288  df-op 4292  df-iun 4630  df-opab 4821
This theorem is referenced by:  marypha2lem2  8458
  Copyright terms: Public domain W3C validator