| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > vtoclbg | Structured version Visualization version GIF version | ||
| Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.) |
| Ref | Expression |
|---|---|
| vtoclbg.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) |
| vtoclbg.2 | ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) |
| vtoclbg.3 | ⊢ (𝜑 ↔ 𝜓) |
| Ref | Expression |
|---|---|
| vtoclbg | ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vtoclbg.1 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) | |
| 2 | vtoclbg.2 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) | |
| 3 | 1, 2 | bibi12d 345 | . 2 ⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ 𝜃))) |
| 4 | vtoclbg.3 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
| 5 | 3, 4 | vtoclg 3554 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ∈ wcel 2108 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-clel 2816 |
| This theorem is referenced by: alexeqg 3651 pm13.183 3666 elab6g 3669 elabgw 3677 sbc8g 3796 sbc2or 3797 sbccow 3811 sbcco 3814 sbc5ALT 3817 sbcie2g 3829 eqsbc1 3835 sbcng 3836 sbcimg 3837 sbcan 3838 sbcor 3839 sbcbig 3840 sbcal 3849 sbcex2 3850 sbcel1v 3856 sbcreu 3876 csbiebg 3931 sbcel12 4411 sbceqg 4412 csbie2df 4443 preq12bg 4853 elintrabg 4961 sbcbr123 5197 inisegn0 6116 fsn2g 7158 funfvima3 7256 elixpsn 8977 ixpsnf1o 8978 domeng 9003 1sdomOLD 9285 rankcf 10817 eldm3 35761 elima4 35776 brsset 35890 brbigcup 35899 elfix2 35905 elfunsg 35917 elsingles 35919 funpartlem 35943 ellines 36153 elhf2g 36177 bj-elpwgALT 37055 cover2g 37723 sbcrexgOLD 42796 |
| Copyright terms: Public domain | W3C validator |