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

Theorem elmptrab 21440
 Description: Membership in a one-parameter class of sets. (Contributed by Stefan O'Rear, 28-Jul-2015.)
Hypotheses
Ref Expression
elmptrab.f 𝐹 = (𝑥𝐷 ↦ {𝑦𝐵𝜑})
elmptrab.s1 ((𝑥 = 𝑋𝑦 = 𝑌) → (𝜑𝜓))
elmptrab.s2 (𝑥 = 𝑋𝐵 = 𝐶)
elmptrab.ex (𝑥𝐷𝐵𝑉)
Assertion
Ref Expression
elmptrab (𝑌 ∈ (𝐹𝑋) ↔ (𝑋𝐷𝑌𝐶𝜓))
Distinct variable groups:   𝑥,𝑦,𝑋   𝑦,𝐵   𝑥,𝐶,𝑦   𝑥,𝐷   𝑥,𝑉,𝑦   𝑥,𝑌,𝑦   𝜓,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐵(𝑥)   𝐷(𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem elmptrab
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elmptrab.f . . 3 𝐹 = (𝑥𝐷 ↦ {𝑦𝐵𝜑})
21mptrcl 6198 . 2 (𝑌 ∈ (𝐹𝑋) → 𝑋𝐷)
3 simp1 1054 . 2 ((𝑋𝐷𝑌𝐶𝜓) → 𝑋𝐷)
4 csbeq1 3502 . . . . . 6 (𝑧 = 𝑋𝑧 / 𝑥𝐵 = 𝑋 / 𝑥𝐵)
5 dfsbcq 3404 . . . . . 6 (𝑧 = 𝑋 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑[𝑋 / 𝑥][𝑤 / 𝑦]𝜑))
64, 5rabeqbidv 3168 . . . . 5 (𝑧 = 𝑋 → {𝑤𝑧 / 𝑥𝐵[𝑧 / 𝑥][𝑤 / 𝑦]𝜑} = {𝑤𝑋 / 𝑥𝐵[𝑋 / 𝑥][𝑤 / 𝑦]𝜑})
7 nfcv 2751 . . . . . . 7 𝑧{𝑦𝐵𝜑}
8 nfsbc1v 3422 . . . . . . . 8 𝑥[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
9 nfcsb1v 3515 . . . . . . . 8 𝑥𝑧 / 𝑥𝐵
108, 9nfrab 3100 . . . . . . 7 𝑥{𝑤𝑧 / 𝑥𝐵[𝑧 / 𝑥][𝑤 / 𝑦]𝜑}
11 csbeq1a 3508 . . . . . . . . 9 (𝑥 = 𝑧𝐵 = 𝑧 / 𝑥𝐵)
12 sbceq1a 3413 . . . . . . . . 9 (𝑥 = 𝑧 → (𝜑[𝑧 / 𝑥]𝜑))
1311, 12rabeqbidv 3168 . . . . . . . 8 (𝑥 = 𝑧 → {𝑦𝐵𝜑} = {𝑦𝑧 / 𝑥𝐵[𝑧 / 𝑥]𝜑})
14 nfcv 2751 . . . . . . . . 9 𝑤𝑧 / 𝑥𝐵
15 nfcv 2751 . . . . . . . . 9 𝑦𝑧 / 𝑥𝐵
16 nfcv 2751 . . . . . . . . . 10 𝑦𝑧
17 nfsbc1v 3422 . . . . . . . . . 10 𝑦[𝑤 / 𝑦]𝜑
1816, 17nfsbc 3424 . . . . . . . . 9 𝑦[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
19 nfv 1830 . . . . . . . . 9 𝑤[𝑧 / 𝑥]𝜑
20 sbceq1a 3413 . . . . . . . . . . 11 (𝑦 = 𝑤 → ([𝑧 / 𝑥]𝜑[𝑤 / 𝑦][𝑧 / 𝑥]𝜑))
2120equcoms 1934 . . . . . . . . . 10 (𝑤 = 𝑦 → ([𝑧 / 𝑥]𝜑[𝑤 / 𝑦][𝑧 / 𝑥]𝜑))
22 sbccom 3476 . . . . . . . . . 10 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑[𝑤 / 𝑦][𝑧 / 𝑥]𝜑)
2321, 22syl6rbbr 278 . . . . . . . . 9 (𝑤 = 𝑦 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑[𝑧 / 𝑥]𝜑))
2414, 15, 18, 19, 23cbvrab 3171 . . . . . . . 8 {𝑤𝑧 / 𝑥𝐵[𝑧 / 𝑥][𝑤 / 𝑦]𝜑} = {𝑦𝑧 / 𝑥𝐵[𝑧 / 𝑥]𝜑}
2513, 24syl6eqr 2662 . . . . . . 7 (𝑥 = 𝑧 → {𝑦𝐵𝜑} = {𝑤𝑧 / 𝑥𝐵[𝑧 / 𝑥][𝑤 / 𝑦]𝜑})
267, 10, 25cbvmpt 4677 . . . . . 6 (𝑥𝐷 ↦ {𝑦𝐵𝜑}) = (𝑧𝐷 ↦ {𝑤𝑧 / 𝑥𝐵[𝑧 / 𝑥][𝑤 / 𝑦]𝜑})
271, 26eqtri 2632 . . . . 5 𝐹 = (𝑧𝐷 ↦ {𝑤𝑧 / 𝑥𝐵[𝑧 / 𝑥][𝑤 / 𝑦]𝜑})
28 nfv 1830 . . . . . . . 8 𝑥 𝑧𝐷
299nfel1 2765 . . . . . . . 8 𝑥𝑧 / 𝑥𝐵𝑉
3028, 29nfim 1813 . . . . . . 7 𝑥(𝑧𝐷𝑧 / 𝑥𝐵𝑉)
31 eleq1 2676 . . . . . . . 8 (𝑥 = 𝑧 → (𝑥𝐷𝑧𝐷))
3211eleq1d 2672 . . . . . . . 8 (𝑥 = 𝑧 → (𝐵𝑉𝑧 / 𝑥𝐵𝑉))
3331, 32imbi12d 333 . . . . . . 7 (𝑥 = 𝑧 → ((𝑥𝐷𝐵𝑉) ↔ (𝑧𝐷𝑧 / 𝑥𝐵𝑉)))
34 elmptrab.ex . . . . . . 7 (𝑥𝐷𝐵𝑉)
3530, 33, 34chvar 2250 . . . . . 6 (𝑧𝐷𝑧 / 𝑥𝐵𝑉)
36 rabexg 4739 . . . . . 6 (𝑧 / 𝑥𝐵𝑉 → {𝑤𝑧 / 𝑥𝐵[𝑧 / 𝑥][𝑤 / 𝑦]𝜑} ∈ V)
3735, 36syl 17 . . . . 5 (𝑧𝐷 → {𝑤𝑧 / 𝑥𝐵[𝑧 / 𝑥][𝑤 / 𝑦]𝜑} ∈ V)
386, 27, 37fvmpt3 6195 . . . 4 (𝑋𝐷 → (𝐹𝑋) = {𝑤𝑋 / 𝑥𝐵[𝑋 / 𝑥][𝑤 / 𝑦]𝜑})
3938eleq2d 2673 . . 3 (𝑋𝐷 → (𝑌 ∈ (𝐹𝑋) ↔ 𝑌 ∈ {𝑤𝑋 / 𝑥𝐵[𝑋 / 𝑥][𝑤 / 𝑦]𝜑}))
40 dfsbcq 3404 . . . . . . 7 (𝑤 = 𝑌 → ([𝑤 / 𝑦]𝜑[𝑌 / 𝑦]𝜑))
4140sbcbidv 3457 . . . . . 6 (𝑤 = 𝑌 → ([𝑋 / 𝑥][𝑤 / 𝑦]𝜑[𝑋 / 𝑥][𝑌 / 𝑦]𝜑))
4241elrab 3331 . . . . 5 (𝑌 ∈ {𝑤𝑋 / 𝑥𝐵[𝑋 / 𝑥][𝑤 / 𝑦]𝜑} ↔ (𝑌𝑋 / 𝑥𝐵[𝑋 / 𝑥][𝑌 / 𝑦]𝜑))
4342a1i 11 . . . 4 (𝑋𝐷 → (𝑌 ∈ {𝑤𝑋 / 𝑥𝐵[𝑋 / 𝑥][𝑤 / 𝑦]𝜑} ↔ (𝑌𝑋 / 𝑥𝐵[𝑋 / 𝑥][𝑌 / 𝑦]𝜑)))
44 nfcvd 2752 . . . . . . 7 (𝑋𝐷𝑥𝐶)
45 elmptrab.s2 . . . . . . 7 (𝑥 = 𝑋𝐵 = 𝐶)
4644, 45csbiegf 3523 . . . . . 6 (𝑋𝐷𝑋 / 𝑥𝐵 = 𝐶)
4746eleq2d 2673 . . . . 5 (𝑋𝐷 → (𝑌𝑋 / 𝑥𝐵𝑌𝐶))
4847anbi1d 737 . . . 4 (𝑋𝐷 → ((𝑌𝑋 / 𝑥𝐵[𝑋 / 𝑥][𝑌 / 𝑦]𝜑) ↔ (𝑌𝐶[𝑋 / 𝑥][𝑌 / 𝑦]𝜑)))
49 nfv 1830 . . . . . 6 𝑥𝜓
50 nfv 1830 . . . . . 6 𝑦𝜓
51 nfv 1830 . . . . . 6 𝑥 𝑌𝐶
52 elmptrab.s1 . . . . . 6 ((𝑥 = 𝑋𝑦 = 𝑌) → (𝜑𝜓))
5349, 50, 51, 52sbc2iegf 3471 . . . . 5 ((𝑋𝐷𝑌𝐶) → ([𝑋 / 𝑥][𝑌 / 𝑦]𝜑𝜓))
5453pm5.32da 671 . . . 4 (𝑋𝐷 → ((𝑌𝐶[𝑋 / 𝑥][𝑌 / 𝑦]𝜑) ↔ (𝑌𝐶𝜓)))
5543, 48, 543bitrd 293 . . 3 (𝑋𝐷 → (𝑌 ∈ {𝑤𝑋 / 𝑥𝐵[𝑋 / 𝑥][𝑤 / 𝑦]𝜑} ↔ (𝑌𝐶𝜓)))
56 3anass 1035 . . . 4 ((𝑋𝐷𝑌𝐶𝜓) ↔ (𝑋𝐷 ∧ (𝑌𝐶𝜓)))
5756baibr 943 . . 3 (𝑋𝐷 → ((𝑌𝐶𝜓) ↔ (𝑋𝐷𝑌𝐶𝜓)))
5839, 55, 573bitrd 293 . 2 (𝑋𝐷 → (𝑌 ∈ (𝐹𝑋) ↔ (𝑋𝐷𝑌𝐶𝜓)))
592, 3, 58pm5.21nii 367 1 (𝑌 ∈ (𝐹𝑋) ↔ (𝑋𝐷𝑌𝐶𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  {crab 2900  Vcvv 3173  [wsbc 3402  ⦋csb 3499   ↦ cmpt 4643  ‘cfv 5804 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fv 5812 This theorem is referenced by:  elmptrab2OLD  21441  elmptrab2  21442  isfbas  21443
 Copyright terms: Public domain W3C validator