Theorem opelopabsb 4985

Description: The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.)

Assertion

Ref	Expression
opelopabsb	⊢ (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)

Distinct variable groups:   𝑥,𝑦   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥,𝑦)   𝐵(𝑦)

Proof of Theorem opelopabsb

Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3203	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
2		vex 3203	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
3	1, 2	opnzi 4943	. . . . . . . . 9 ⊢ ⟨𝑥, 𝑦⟩ ≠ ∅
4		simpl 473	. . . . . . . . . . 11 ⊢ ((∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ∅ = ⟨𝑥, 𝑦⟩)
5	4	eqcomd 2628	. . . . . . . . . 10 ⊢ ((∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ⟨𝑥, 𝑦⟩ = ∅)
6	5	necon3ai 2819	. . . . . . . . 9 ⊢ (⟨𝑥, 𝑦⟩ ≠ ∅ → ¬ (∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
7	3, 6	ax-mp 5	. . . . . . . 8 ⊢ ¬ (∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
8	7	nex 1731	. . . . . . 7 ⊢ ¬ ∃𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
9	8	nex 1731	. . . . . 6 ⊢ ¬ ∃𝑥∃𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
10		elopab 4983	. . . . . 6 ⊢ (∅ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
11	9, 10	mtbir 313	. . . . 5 ⊢ ¬ ∅ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}
12		eleq1 2689	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ∅ → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∅ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}))
13	11, 12	mtbiri 317	. . . 4 ⊢ (⟨𝐴, 𝐵⟩ = ∅ → ¬ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
14	13	necon2ai 2823	. . 3 ⊢ (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} → ⟨𝐴, 𝐵⟩ ≠ ∅)
15		opnz 4942	. . 3 ⊢ (⟨𝐴, 𝐵⟩ ≠ ∅ ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V))
16	14, 15	sylib 208	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} → (𝐴 ∈ V ∧ 𝐵 ∈ V))
17		sbcex 3445	. . 3 ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 → 𝐴 ∈ V)
18		spesbc 3521	. . . 4 ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 → ∃𝑥[𝐵 / 𝑦]𝜑)
19		sbcex 3445	. . . . 5 ⊢ ([𝐵 / 𝑦]𝜑 → 𝐵 ∈ V)
20	19	exlimiv 1858	. . . 4 ⊢ (∃𝑥[𝐵 / 𝑦]𝜑 → 𝐵 ∈ V)
21	18, 20	syl 17	. . 3 ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 → 𝐵 ∈ V)
22	17, 21	jca 554	. 2 ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
23		opeq1 4402	. . . . 5 ⊢ (𝑧 = 𝐴 → ⟨𝑧, 𝑤⟩ = ⟨𝐴, 𝑤⟩)
24	23	eleq1d 2686	. . . 4 ⊢ (𝑧 = 𝐴 → (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ⟨𝐴, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}))
25		dfsbcq2 3438	. . . 4 ⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝐴 / 𝑥][𝑤 / 𝑦]𝜑))
26	24, 25	bibi12d 335	. . 3 ⊢ (𝑧 = 𝐴 → ((⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) ↔ (⟨𝐴, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝑤 / 𝑦]𝜑)))
27		opeq2 4403	. . . . 5 ⊢ (𝑤 = 𝐵 → ⟨𝐴, 𝑤⟩ = ⟨𝐴, 𝐵⟩)
28	27	eleq1d 2686	. . . 4 ⊢ (𝑤 = 𝐵 → (⟨𝐴, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}))
29		dfsbcq2 3438	. . . . 5 ⊢ (𝑤 = 𝐵 → ([𝑤 / 𝑦]𝜑 ↔ [𝐵 / 𝑦]𝜑))
30	29	sbcbidv 3490	. . . 4 ⊢ (𝑤 = 𝐵 → ([𝐴 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑))
31	28, 30	bibi12d 335	. . 3 ⊢ (𝑤 = 𝐵 → ((⟨𝐴, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝑤 / 𝑦]𝜑) ↔ (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)))
32		nfopab1 4719	. . . . . 6 ⊢ Ⅎ𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}
33	32	nfel2 2781	. . . . 5 ⊢ Ⅎ𝑥⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}
34		nfs1v 2437	. . . . 5 ⊢ Ⅎ𝑥[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
35	33, 34	nfbi 1833	. . . 4 ⊢ Ⅎ𝑥(⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)
36		opeq1 4402	. . . . . 6 ⊢ (𝑥 = 𝑧 → ⟨𝑥, 𝑤⟩ = ⟨𝑧, 𝑤⟩)
37	36	eleq1d 2686	. . . . 5 ⊢ (𝑥 = 𝑧 → (⟨𝑥, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}))
38		sbequ12 2111	. . . . 5 ⊢ (𝑥 = 𝑧 → ([𝑤 / 𝑦]𝜑 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑))
39	37, 38	bibi12d 335	. . . 4 ⊢ (𝑥 = 𝑧 → ((⟨𝑥, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑤 / 𝑦]𝜑) ↔ (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)))
40		nfopab2 4720	. . . . . . 7 ⊢ Ⅎ𝑦{⟨𝑥, 𝑦⟩ ∣ 𝜑}
41	40	nfel2 2781	. . . . . 6 ⊢ Ⅎ𝑦⟨𝑥, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}
42		nfs1v 2437	. . . . . 6 ⊢ Ⅎ𝑦[𝑤 / 𝑦]𝜑
43	41, 42	nfbi 1833	. . . . 5 ⊢ Ⅎ𝑦(⟨𝑥, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑤 / 𝑦]𝜑)
44		opeq2 4403	. . . . . . 7 ⊢ (𝑦 = 𝑤 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑤⟩)
45	44	eleq1d 2686	. . . . . 6 ⊢ (𝑦 = 𝑤 → (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ⟨𝑥, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}))
46		sbequ12 2111	. . . . . 6 ⊢ (𝑦 = 𝑤 → (𝜑 ↔ [𝑤 / 𝑦]𝜑))
47	45, 46	bibi12d 335	. . . . 5 ⊢ (𝑦 = 𝑤 → ((⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑) ↔ (⟨𝑥, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑤 / 𝑦]𝜑)))
48		opabid 4982	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)
49	43, 47, 48	chvar 2262	. . . 4 ⊢ (⟨𝑥, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑤 / 𝑦]𝜑)
50	35, 39, 49	chvar 2262	. . 3 ⊢ (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)
51	26, 31, 50	vtocl2g 3270	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑))
52	16, 22, 51	pm5.21nii 368	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 196   ∧ wa 384   = wceq 1483  ∃wex 1704  [wsb 1880   ∈ wcel 1990   ≠ wne 2794  Vcvv 3200  [wsbc 3435  ∅c0 3915  ⟨cop 4183  {copab 4712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-opab 4713

This theorem is referenced by:  brabsb  4986  opelopabgf  4995  opelopabaf  4999  opelopabf  5000  difopab  5253  isarep1  5977  fmptsnd  6435