Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elrabf | Structured version Visualization version GIF version |
Description: Membership in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003.) |
Ref | Expression |
---|---|
elrabf.1 | ⊢ Ⅎ𝑥𝐴 |
elrabf.2 | ⊢ Ⅎ𝑥𝐵 |
elrabf.3 | ⊢ Ⅎ𝑥𝜓 |
elrabf.4 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
elrabf | ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3416 | . 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} → 𝐴 ∈ V) | |
2 | elex 3416 | . . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V) | |
3 | 2 | adantr 484 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → 𝐴 ∈ V) |
4 | df-rab 3062 | . . . 4 ⊢ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} | |
5 | 4 | eleq2i 2824 | . . 3 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)}) |
6 | elrabf.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
7 | elrabf.2 | . . . . . 6 ⊢ Ⅎ𝑥𝐵 | |
8 | 6, 7 | nfel 2913 | . . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 |
9 | elrabf.3 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
10 | 8, 9 | nfan 1906 | . . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 ∧ 𝜓) |
11 | eleq1 2820 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
12 | elrabf.4 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
13 | 11, 12 | anbi12d 634 | . . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))) |
14 | 6, 10, 13 | elabgf 3568 | . . 3 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))) |
15 | 5, 14 | syl5bb 286 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))) |
16 | 1, 3, 15 | pm5.21nii 383 | 1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1542 Ⅎwnf 1790 ∈ wcel 2114 {cab 2716 Ⅎwnfc 2879 {crab 3057 Vcvv 3398 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-tru 1545 df-ex 1787 df-nf 1791 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-rab 3062 df-v 3400 |
This theorem is referenced by: rabtru 3585 invdisjrabw 5015 invdisjrab 5016 rabxfrd 5284 f1ossf1o 6900 onminsb 7533 nnawordex 8294 tskwe 9452 rabssnn0fi 13445 iundisj 24300 iundisjf 30502 iundisjfi 30692 bnj1388 32584 sltval2 33500 phpreu 35384 poimirlem26 35426 sticksstones1 39708 rfcnpre3 42114 rfcnpre4 42115 uzwo4 42139 disjinfi 42269 allbutfiinf 42498 fsumiunss 42658 fnlimfvre 42757 stoweidlem26 43109 stoweidlem27 43110 stoweidlem31 43114 stoweidlem34 43117 stoweidlem51 43134 stoweidlem52 43135 stoweidlem59 43142 fourierdlem20 43210 fourierdlem79 43268 pimdecfgtioc 43791 smfpimcclem 43879 prmdvdsfmtnof1lem1 44570 |
Copyright terms: Public domain | W3C validator |