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

Theorem opeliunxp 4603
 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 2701 . 2 (⟨𝑥, 𝐶⟩ ∈ 𝑥𝐴 ({𝑥} × 𝐵) → ⟨𝑥, 𝐶⟩ ∈ V)
2 opexg 4159 . 2 ((𝑥𝐴𝐶𝐵) → ⟨𝑥, 𝐶⟩ ∈ V)
3 df-rex 2423 . . . . . 6 (∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵) ↔ ∃𝑥(𝑥𝐴𝑦 ∈ ({𝑥} × 𝐵)))
4 nfv 1509 . . . . . . 7 𝑧(𝑥𝐴𝑦 ∈ ({𝑥} × 𝐵))
5 nfs1v 1913 . . . . . . . 8 𝑥[𝑧 / 𝑥]𝑥𝐴
6 nfcv 2282 . . . . . . . . . 10 𝑥{𝑧}
7 nfcsb1v 3041 . . . . . . . . . 10 𝑥𝑧 / 𝑥𝐵
86, 7nfxp 4575 . . . . . . . . 9 𝑥({𝑧} × 𝑧 / 𝑥𝐵)
98nfcri 2276 . . . . . . . 8 𝑥 𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵)
105, 9nfan 1545 . . . . . . 7 𝑥([𝑧 / 𝑥]𝑥𝐴𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵))
11 sbequ12 1745 . . . . . . . 8 (𝑥 = 𝑧 → (𝑥𝐴 ↔ [𝑧 / 𝑥]𝑥𝐴))
12 sneq 3544 . . . . . . . . . 10 (𝑥 = 𝑧 → {𝑥} = {𝑧})
13 csbeq1a 3017 . . . . . . . . . 10 (𝑥 = 𝑧𝐵 = 𝑧 / 𝑥𝐵)
1412, 13xpeq12d 4573 . . . . . . . . 9 (𝑥 = 𝑧 → ({𝑥} × 𝐵) = ({𝑧} × 𝑧 / 𝑥𝐵))
1514eleq2d 2210 . . . . . . . 8 (𝑥 = 𝑧 → (𝑦 ∈ ({𝑥} × 𝐵) ↔ 𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵)))
1611, 15anbi12d 465 . . . . . . 7 (𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∈ ({𝑥} × 𝐵)) ↔ ([𝑧 / 𝑥]𝑥𝐴𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵))))
174, 10, 16cbvex 1730 . . . . . 6 (∃𝑥(𝑥𝐴𝑦 ∈ ({𝑥} × 𝐵)) ↔ ∃𝑧([𝑧 / 𝑥]𝑥𝐴𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵)))
183, 17bitri 183 . . . . 5 (∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵) ↔ ∃𝑧([𝑧 / 𝑥]𝑥𝐴𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵)))
19 eleq1 2203 . . . . . . 7 (𝑦 = ⟨𝑥, 𝐶⟩ → (𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵) ↔ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵)))
2019anbi2d 460 . . . . . 6 (𝑦 = ⟨𝑥, 𝐶⟩ → (([𝑧 / 𝑥]𝑥𝐴𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵)) ↔ ([𝑧 / 𝑥]𝑥𝐴 ∧ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵))))
2120exbidv 1798 . . . . 5 (𝑦 = ⟨𝑥, 𝐶⟩ → (∃𝑧([𝑧 / 𝑥]𝑥𝐴𝑦 ∈ ({𝑧} × 𝑧 / 𝑥𝐵)) ↔ ∃𝑧([𝑧 / 𝑥]𝑥𝐴 ∧ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵))))
2218, 21syl5bb 191 . . . 4 (𝑦 = ⟨𝑥, 𝐶⟩ → (∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵) ↔ ∃𝑧([𝑧 / 𝑥]𝑥𝐴 ∧ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵))))
23 df-iun 3824 . . . 4 𝑥𝐴 ({𝑥} × 𝐵) = {𝑦 ∣ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵)}
2422, 23elab2g 2836 . . 3 (⟨𝑥, 𝐶⟩ ∈ V → (⟨𝑥, 𝐶⟩ ∈ 𝑥𝐴 ({𝑥} × 𝐵) ↔ ∃𝑧([𝑧 / 𝑥]𝑥𝐴 ∧ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵))))
25 opelxp 4578 . . . . . . 7 (⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵) ↔ (𝑥 ∈ {𝑧} ∧ 𝐶𝑧 / 𝑥𝐵))
2625anbi2i 453 . . . . . 6 (([𝑧 / 𝑥]𝑥𝐴 ∧ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵)) ↔ ([𝑧 / 𝑥]𝑥𝐴 ∧ (𝑥 ∈ {𝑧} ∧ 𝐶𝑧 / 𝑥𝐵)))
27 an12 551 . . . . . 6 (([𝑧 / 𝑥]𝑥𝐴 ∧ (𝑥 ∈ {𝑧} ∧ 𝐶𝑧 / 𝑥𝐵)) ↔ (𝑥 ∈ {𝑧} ∧ ([𝑧 / 𝑥]𝑥𝐴𝐶𝑧 / 𝑥𝐵)))
28 velsn 3550 . . . . . . . 8 (𝑥 ∈ {𝑧} ↔ 𝑥 = 𝑧)
29 equcom 1683 . . . . . . . 8 (𝑥 = 𝑧𝑧 = 𝑥)
3028, 29bitri 183 . . . . . . 7 (𝑥 ∈ {𝑧} ↔ 𝑧 = 𝑥)
3130anbi1i 454 . . . . . 6 ((𝑥 ∈ {𝑧} ∧ ([𝑧 / 𝑥]𝑥𝐴𝐶𝑧 / 𝑥𝐵)) ↔ (𝑧 = 𝑥 ∧ ([𝑧 / 𝑥]𝑥𝐴𝐶𝑧 / 𝑥𝐵)))
3226, 27, 313bitri 205 . . . . 5 (([𝑧 / 𝑥]𝑥𝐴 ∧ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵)) ↔ (𝑧 = 𝑥 ∧ ([𝑧 / 𝑥]𝑥𝐴𝐶𝑧 / 𝑥𝐵)))
3332exbii 1585 . . . 4 (∃𝑧([𝑧 / 𝑥]𝑥𝐴 ∧ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵)) ↔ ∃𝑧(𝑧 = 𝑥 ∧ ([𝑧 / 𝑥]𝑥𝐴𝐶𝑧 / 𝑥𝐵)))
34 vex 2693 . . . . 5 𝑥 ∈ V
35 sbequ12r 1746 . . . . . 6 (𝑧 = 𝑥 → ([𝑧 / 𝑥]𝑥𝐴𝑥𝐴))
3613equcoms 1685 . . . . . . . 8 (𝑧 = 𝑥𝐵 = 𝑧 / 𝑥𝐵)
3736eqcomd 2146 . . . . . . 7 (𝑧 = 𝑥𝑧 / 𝑥𝐵 = 𝐵)
3837eleq2d 2210 . . . . . 6 (𝑧 = 𝑥 → (𝐶𝑧 / 𝑥𝐵𝐶𝐵))
3935, 38anbi12d 465 . . . . 5 (𝑧 = 𝑥 → (([𝑧 / 𝑥]𝑥𝐴𝐶𝑧 / 𝑥𝐵) ↔ (𝑥𝐴𝐶𝐵)))
4034, 39ceqsexv 2729 . . . 4 (∃𝑧(𝑧 = 𝑥 ∧ ([𝑧 / 𝑥]𝑥𝐴𝐶𝑧 / 𝑥𝐵)) ↔ (𝑥𝐴𝐶𝐵))
4133, 40bitri 183 . . 3 (∃𝑧([𝑧 / 𝑥]𝑥𝐴 ∧ ⟨𝑥, 𝐶⟩ ∈ ({𝑧} × 𝑧 / 𝑥𝐵)) ↔ (𝑥𝐴𝐶𝐵))
4224, 41syl6bb 195 . 2 (⟨𝑥, 𝐶⟩ ∈ V → (⟨𝑥, 𝐶⟩ ∈ 𝑥𝐴 ({𝑥} × 𝐵) ↔ (𝑥𝐴𝐶𝐵)))
431, 2, 42pm5.21nii 694 1 (⟨𝑥, 𝐶⟩ ∈ 𝑥𝐴 ({𝑥} × 𝐵) ↔ (𝑥𝐴𝐶𝐵))
 Colors of variables: wff set class Syntax hints:   ∧ wa 103   ↔ wb 104   = wceq 1332  ∃wex 1469   ∈ wcel 1481  [wsb 1736  ∃wrex 2418  Vcvv 2690  ⦋csb 3008  {csn 3533  ⟨cop 3536  ∪ ciun 3822   × cxp 4546 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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4055  ax-pow 4107  ax-pr 4140 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-v 2692  df-sbc 2915  df-csb 3009  df-un 3081  df-in 3083  df-ss 3090  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-iun 3824  df-opab 3999  df-xp 4554 This theorem is referenced by:  eliunxp  4687  opeliunxp2  4688  opeliunxp2f  6144
 Copyright terms: Public domain W3C validator