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

Theorem opeliunxp 4532
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 2652 . 2 (⟨𝑥, 𝐶⟩ ∈ 𝑥𝐴 ({𝑥} × 𝐵) → ⟨𝑥, 𝐶⟩ ∈ V)
2 opexg 4088 . 2 ((𝑥𝐴𝐶𝐵) → ⟨𝑥, 𝐶⟩ ∈ V)
3 df-rex 2381 . . . . . 6 (∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵) ↔ ∃𝑥(𝑥𝐴𝑦 ∈ ({𝑥} × 𝐵)))
4 nfv 1476 . . . . . . 7 𝑧(𝑥𝐴𝑦 ∈ ({𝑥} × 𝐵))
5 nfs1v 1875 . . . . . . . 8 𝑥[𝑧 / 𝑥]𝑥𝐴
6 nfcv 2240 . . . . . . . . . 10 𝑥{𝑧}
7 nfcsb1v 2985 . . . . . . . . . 10 𝑥𝑧 / 𝑥𝐵
86, 7nfxp 4504 . . . . . . . . 9 𝑥({𝑧} × 𝑧 / 𝑥𝐵)
98nfcri 2234 . . . . . . . 8 𝑥 𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵)
105, 9nfan 1512 . . . . . . 7 𝑥([𝑧 / 𝑥]𝑥𝐴𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵))
11 sbequ12 1712 . . . . . . . 8 (𝑥 = 𝑧 → (𝑥𝐴 ↔ [𝑧 / 𝑥]𝑥𝐴))
12 sneq 3485 . . . . . . . . . 10 (𝑥 = 𝑧 → {𝑥} = {𝑧})
13 csbeq1a 2963 . . . . . . . . . 10 (𝑥 = 𝑧𝐵 = 𝑧 / 𝑥𝐵)
1412, 13xpeq12d 4502 . . . . . . . . 9 (𝑥 = 𝑧 → ({𝑥} × 𝐵) = ({𝑧} × 𝑧 / 𝑥𝐵))
1514eleq2d 2169 . . . . . . . 8 (𝑥 = 𝑧 → (𝑦 ∈ ({𝑥} × 𝐵) ↔ 𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵)))
1611, 15anbi12d 460 . . . . . . 7 (𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∈ ({𝑥} × 𝐵)) ↔ ([𝑧 / 𝑥]𝑥𝐴𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵))))
174, 10, 16cbvex 1697 . . . . . 6 (∃𝑥(𝑥𝐴𝑦 ∈ ({𝑥} × 𝐵)) ↔ ∃𝑧([𝑧 / 𝑥]𝑥𝐴𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵)))
183, 17bitri 183 . . . . 5 (∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵) ↔ ∃𝑧([𝑧 / 𝑥]𝑥𝐴𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵)))
19 eleq1 2162 . . . . . . 7 (𝑦 = ⟨𝑥, 𝐶⟩ → (𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵) ↔ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵)))
2019anbi2d 455 . . . . . 6 (𝑦 = ⟨𝑥, 𝐶⟩ → (([𝑧 / 𝑥]𝑥𝐴𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵)) ↔ ([𝑧 / 𝑥]𝑥𝐴 ∧ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵))))
2120exbidv 1764 . . . . 5 (𝑦 = ⟨𝑥, 𝐶⟩ → (∃𝑧([𝑧 / 𝑥]𝑥𝐴𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵)) ↔ ∃𝑧([𝑧 / 𝑥]𝑥𝐴 ∧ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵))))
2218, 21syl5bb 191 . . . 4 (𝑦 = ⟨𝑥, 𝐶⟩ → (∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵) ↔ ∃𝑧([𝑧 / 𝑥]𝑥𝐴 ∧ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵))))
23 df-iun 3762 . . . 4 𝑥𝐴 ({𝑥} × 𝐵) = {𝑦 ∣ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵)}
2422, 23elab2g 2784 . . 3 (⟨𝑥, 𝐶⟩ ∈ V → (⟨𝑥, 𝐶⟩ ∈ 𝑥𝐴 ({𝑥} × 𝐵) ↔ ∃𝑧([𝑧 / 𝑥]𝑥𝐴 ∧ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵))))
25 opelxp 4507 . . . . . . 7 (⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵) ↔ (𝑥 ∈ {𝑧} ∧ 𝐶𝑧 / 𝑥𝐵))
2625anbi2i 448 . . . . . 6 (([𝑧 / 𝑥]𝑥𝐴 ∧ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵)) ↔ ([𝑧 / 𝑥]𝑥𝐴 ∧ (𝑥 ∈ {𝑧} ∧ 𝐶𝑧 / 𝑥𝐵)))
27 an12 531 . . . . . 6 (([𝑧 / 𝑥]𝑥𝐴 ∧ (𝑥 ∈ {𝑧} ∧ 𝐶𝑧 / 𝑥𝐵)) ↔ (𝑥 ∈ {𝑧} ∧ ([𝑧 / 𝑥]𝑥𝐴𝐶𝑧 / 𝑥𝐵)))
28 velsn 3491 . . . . . . . 8 (𝑥 ∈ {𝑧} ↔ 𝑥 = 𝑧)
29 equcom 1650 . . . . . . . 8 (𝑥 = 𝑧𝑧 = 𝑥)
3028, 29bitri 183 . . . . . . 7 (𝑥 ∈ {𝑧} ↔ 𝑧 = 𝑥)
3130anbi1i 449 . . . . . 6 ((𝑥 ∈ {𝑧} ∧ ([𝑧 / 𝑥]𝑥𝐴𝐶𝑧 / 𝑥𝐵)) ↔ (𝑧 = 𝑥 ∧ ([𝑧 / 𝑥]𝑥𝐴𝐶𝑧 / 𝑥𝐵)))
3226, 27, 313bitri 205 . . . . 5 (([𝑧 / 𝑥]𝑥𝐴 ∧ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵)) ↔ (𝑧 = 𝑥 ∧ ([𝑧 / 𝑥]𝑥𝐴𝐶𝑧 / 𝑥𝐵)))
3332exbii 1552 . . . 4 (∃𝑧([𝑧 / 𝑥]𝑥𝐴 ∧ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵)) ↔ ∃𝑧(𝑧 = 𝑥 ∧ ([𝑧 / 𝑥]𝑥𝐴𝐶𝑧 / 𝑥𝐵)))
34 vex 2644 . . . . 5 𝑥 ∈ V
35 sbequ12r 1713 . . . . . 6 (𝑧 = 𝑥 → ([𝑧 / 𝑥]𝑥𝐴𝑥𝐴))
3613equcoms 1652 . . . . . . . 8 (𝑧 = 𝑥𝐵 = 𝑧 / 𝑥𝐵)
3736eqcomd 2105 . . . . . . 7 (𝑧 = 𝑥𝑧 / 𝑥𝐵 = 𝐵)
3837eleq2d 2169 . . . . . 6 (𝑧 = 𝑥 → (𝐶𝑧 / 𝑥𝐵𝐶𝐵))
3935, 38anbi12d 460 . . . . 5 (𝑧 = 𝑥 → (([𝑧 / 𝑥]𝑥𝐴𝐶𝑧 / 𝑥𝐵) ↔ (𝑥𝐴𝐶𝐵)))
4034, 39ceqsexv 2680 . . . 4 (∃𝑧(𝑧 = 𝑥 ∧ ([𝑧 / 𝑥]𝑥𝐴𝐶𝑧 / 𝑥𝐵)) ↔ (𝑥𝐴𝐶𝐵))
4133, 40bitri 183 . . 3 (∃𝑧([𝑧 / 𝑥]𝑥𝐴 ∧ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵)) ↔ (𝑥𝐴𝐶𝐵))
4224, 41syl6bb 195 . 2 (⟨𝑥, 𝐶⟩ ∈ V → (⟨𝑥, 𝐶⟩ ∈ 𝑥𝐴 ({𝑥} × 𝐵) ↔ (𝑥𝐴𝐶𝐵)))
431, 2, 42pm5.21nii 661 1 (⟨𝑥, 𝐶⟩ ∈ 𝑥𝐴 ({𝑥} × 𝐵) ↔ (𝑥𝐴𝐶𝐵))
Colors of variables: wff set class
Syntax hints:  wa 103  wb 104   = wceq 1299  wex 1436  wcel 1448  [wsb 1703  wrex 2376  Vcvv 2641  csb 2955  {csn 3474  cop 3477   ciun 3760   × cxp 4475
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-14 1460  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-sep 3986  ax-pow 4038  ax-pr 4069
This theorem depends on definitions:  df-bi 116  df-3an 932  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ral 2380  df-rex 2381  df-v 2643  df-sbc 2863  df-csb 2956  df-un 3025  df-in 3027  df-ss 3034  df-pw 3459  df-sn 3480  df-pr 3481  df-op 3483  df-iun 3762  df-opab 3930  df-xp 4483
This theorem is referenced by:  eliunxp  4616  opeliunxp2  4617  opeliunxp2f  6065
  Copyright terms: Public domain W3C validator