ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  opeliunxp GIF version

Theorem opeliunxp 4675
Description: Membership in a union of cross products. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Mario Carneiro, 1-Jan-2017.)
Assertion
Ref Expression
opeliunxp (⟨𝑥, 𝐶⟩ ∈ 𝑥𝐴 ({𝑥} × 𝐵) ↔ (𝑥𝐴𝐶𝐵))

Proof of Theorem opeliunxp
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 2746 . 2 (⟨𝑥, 𝐶⟩ ∈ 𝑥𝐴 ({𝑥} × 𝐵) → ⟨𝑥, 𝐶⟩ ∈ V)
2 opexg 4222 . 2 ((𝑥𝐴𝐶𝐵) → ⟨𝑥, 𝐶⟩ ∈ V)
3 df-rex 2459 . . . . . 6 (∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵) ↔ ∃𝑥(𝑥𝐴𝑦 ∈ ({𝑥} × 𝐵)))
4 nfv 1526 . . . . . . 7 𝑧(𝑥𝐴𝑦 ∈ ({𝑥} × 𝐵))
5 nfs1v 1937 . . . . . . . 8 𝑥[𝑧 / 𝑥]𝑥𝐴
6 nfcv 2317 . . . . . . . . . 10 𝑥{𝑧}
7 nfcsb1v 3088 . . . . . . . . . 10 𝑥𝑧 / 𝑥𝐵
86, 7nfxp 4647 . . . . . . . . 9 𝑥({𝑧} × 𝑧 / 𝑥𝐵)
98nfcri 2311 . . . . . . . 8 𝑥 𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵)
105, 9nfan 1563 . . . . . . 7 𝑥([𝑧 / 𝑥]𝑥𝐴𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵))
11 sbequ12 1769 . . . . . . . 8 (𝑥 = 𝑧 → (𝑥𝐴 ↔ [𝑧 / 𝑥]𝑥𝐴))
12 sneq 3600 . . . . . . . . . 10 (𝑥 = 𝑧 → {𝑥} = {𝑧})
13 csbeq1a 3064 . . . . . . . . . 10 (𝑥 = 𝑧𝐵 = 𝑧 / 𝑥𝐵)
1412, 13xpeq12d 4645 . . . . . . . . 9 (𝑥 = 𝑧 → ({𝑥} × 𝐵) = ({𝑧} × 𝑧 / 𝑥𝐵))
1514eleq2d 2245 . . . . . . . 8 (𝑥 = 𝑧 → (𝑦 ∈ ({𝑥} × 𝐵) ↔ 𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵)))
1611, 15anbi12d 473 . . . . . . 7 (𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∈ ({𝑥} × 𝐵)) ↔ ([𝑧 / 𝑥]𝑥𝐴𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵))))
174, 10, 16cbvex 1754 . . . . . 6 (∃𝑥(𝑥𝐴𝑦 ∈ ({𝑥} × 𝐵)) ↔ ∃𝑧([𝑧 / 𝑥]𝑥𝐴𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵)))
183, 17bitri 184 . . . . 5 (∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵) ↔ ∃𝑧([𝑧 / 𝑥]𝑥𝐴𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵)))
19 eleq1 2238 . . . . . . 7 (𝑦 = ⟨𝑥, 𝐶⟩ → (𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵) ↔ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵)))
2019anbi2d 464 . . . . . 6 (𝑦 = ⟨𝑥, 𝐶⟩ → (([𝑧 / 𝑥]𝑥𝐴𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵)) ↔ ([𝑧 / 𝑥]𝑥𝐴 ∧ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵))))
2120exbidv 1823 . . . . 5 (𝑦 = ⟨𝑥, 𝐶⟩ → (∃𝑧([𝑧 / 𝑥]𝑥𝐴𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵)) ↔ ∃𝑧([𝑧 / 𝑥]𝑥𝐴 ∧ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵))))
2218, 21bitrid 192 . . . 4 (𝑦 = ⟨𝑥, 𝐶⟩ → (∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵) ↔ ∃𝑧([𝑧 / 𝑥]𝑥𝐴 ∧ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵))))
23 df-iun 3884 . . . 4 𝑥𝐴 ({𝑥} × 𝐵) = {𝑦 ∣ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵)}
2422, 23elab2g 2882 . . 3 (⟨𝑥, 𝐶⟩ ∈ V → (⟨𝑥, 𝐶⟩ ∈ 𝑥𝐴 ({𝑥} × 𝐵) ↔ ∃𝑧([𝑧 / 𝑥]𝑥𝐴 ∧ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵))))
25 opelxp 4650 . . . . . . 7 (⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵) ↔ (𝑥 ∈ {𝑧} ∧ 𝐶𝑧 / 𝑥𝐵))
2625anbi2i 457 . . . . . 6 (([𝑧 / 𝑥]𝑥𝐴 ∧ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵)) ↔ ([𝑧 / 𝑥]𝑥𝐴 ∧ (𝑥 ∈ {𝑧} ∧ 𝐶𝑧 / 𝑥𝐵)))
27 an12 561 . . . . . 6 (([𝑧 / 𝑥]𝑥𝐴 ∧ (𝑥 ∈ {𝑧} ∧ 𝐶𝑧 / 𝑥𝐵)) ↔ (𝑥 ∈ {𝑧} ∧ ([𝑧 / 𝑥]𝑥𝐴𝐶𝑧 / 𝑥𝐵)))
28 velsn 3606 . . . . . . . 8 (𝑥 ∈ {𝑧} ↔ 𝑥 = 𝑧)
29 equcom 1704 . . . . . . . 8 (𝑥 = 𝑧𝑧 = 𝑥)
3028, 29bitri 184 . . . . . . 7 (𝑥 ∈ {𝑧} ↔ 𝑧 = 𝑥)
3130anbi1i 458 . . . . . 6 ((𝑥 ∈ {𝑧} ∧ ([𝑧 / 𝑥]𝑥𝐴𝐶𝑧 / 𝑥𝐵)) ↔ (𝑧 = 𝑥 ∧ ([𝑧 / 𝑥]𝑥𝐴𝐶𝑧 / 𝑥𝐵)))
3226, 27, 313bitri 206 . . . . 5 (([𝑧 / 𝑥]𝑥𝐴 ∧ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵)) ↔ (𝑧 = 𝑥 ∧ ([𝑧 / 𝑥]𝑥𝐴𝐶𝑧 / 𝑥𝐵)))
3332exbii 1603 . . . 4 (∃𝑧([𝑧 / 𝑥]𝑥𝐴 ∧ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵)) ↔ ∃𝑧(𝑧 = 𝑥 ∧ ([𝑧 / 𝑥]𝑥𝐴𝐶𝑧 / 𝑥𝐵)))
34 vex 2738 . . . . 5 𝑥 ∈ V
35 sbequ12r 1770 . . . . . 6 (𝑧 = 𝑥 → ([𝑧 / 𝑥]𝑥𝐴𝑥𝐴))
3613equcoms 1706 . . . . . . . 8 (𝑧 = 𝑥𝐵 = 𝑧 / 𝑥𝐵)
3736eqcomd 2181 . . . . . . 7 (𝑧 = 𝑥𝑧 / 𝑥𝐵 = 𝐵)
3837eleq2d 2245 . . . . . 6 (𝑧 = 𝑥 → (𝐶𝑧 / 𝑥𝐵𝐶𝐵))
3935, 38anbi12d 473 . . . . 5 (𝑧 = 𝑥 → (([𝑧 / 𝑥]𝑥𝐴𝐶𝑧 / 𝑥𝐵) ↔ (𝑥𝐴𝐶𝐵)))
4034, 39ceqsexv 2774 . . . 4 (∃𝑧(𝑧 = 𝑥 ∧ ([𝑧 / 𝑥]𝑥𝐴𝐶𝑧 / 𝑥𝐵)) ↔ (𝑥𝐴𝐶𝐵))
4133, 40bitri 184 . . 3 (∃𝑧([𝑧 / 𝑥]𝑥𝐴 ∧ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵)) ↔ (𝑥𝐴𝐶𝐵))
4224, 41bitrdi 196 . 2 (⟨𝑥, 𝐶⟩ ∈ V → (⟨𝑥, 𝐶⟩ ∈ 𝑥𝐴 ({𝑥} × 𝐵) ↔ (𝑥𝐴𝐶𝐵)))
431, 2, 42pm5.21nii 704 1 (⟨𝑥, 𝐶⟩ ∈ 𝑥𝐴 ({𝑥} × 𝐵) ↔ (𝑥𝐴𝐶𝐵))
Colors of variables: wff set class
Syntax hints:  wa 104  wb 105   = wceq 1353  wex 1490  [wsb 1760  wcel 2146  wrex 2454  Vcvv 2735  csb 3055  {csn 3589  cop 3592   ciun 3882   × cxp 4618
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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-14 2149  ax-ext 2157  ax-sep 4116  ax-pow 4169  ax-pr 4203
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ral 2458  df-rex 2459  df-v 2737  df-sbc 2961  df-csb 3056  df-un 3131  df-in 3133  df-ss 3140  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-iun 3884  df-opab 4060  df-xp 4626
This theorem is referenced by:  eliunxp  4759  opeliunxp2  4760  opeliunxp2f  6229
  Copyright terms: Public domain W3C validator